\begin{tabbing}
$\forall$$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl(${\it ds}$;${\it da}$), ${\it snd}$:msg{-}spec(${\it ds}$;${\it da}$), $T$:Type.
\\[0ex]($\forall$$k$:Knd. ($k$ $\in$ ecl{-}trans{-}ks(ecl{-}trans($A$))) $\Rightarrow$ $k$ $\in$ dom(${\it da}$))
\\[0ex]$\Rightarrow$ $\neg$"ecl" $\in$ dom(${\it ds}$)
\\[0ex]$\Rightarrow$ $T$ $=$ ecl{-}trans{-}type(ecl{-}trans($A$))
\\[0ex]$\Rightarrow$ e\=cl{-}machine1\=\{ecl:ut2\}\+\+
\\[0ex]($i$; ${\it ds}$; ${\it da}$; $A$) $\parallel$
\-\\[0ex]ecl{-}machine3(${\it ds}$;${\it da}$;"ecl";$T$;ecl{-}trans{-}ks(ecl{-}trans($A$));ecl{-}trans{-}a(ecl{-}trans($A$));${\it snd}$)
\-
\end{tabbing}